;;---------------------------------------------------------------------
;;
;;  P R O J E C T  2 :  T I N Y   T Y P E   R E C O N S T R U C T I O N
;;
;;                      CS515  Ulrich Kremer
;;                           Fall 2011
;;---------------------------------------------------------------------
;;Author: Maurya Talisetti
(require racket/trace)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                             Parser
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define CurrentCounter 0)

(define newtvar
   (lambda()
      (set! CurrentCounter (+ CurrentCounter 1))
      (string->symbol (string-append "_a" (number->string CurrentCounter)))))

(define name?
  (lambda (s)
    (and (symbol? s)
         (not (memq s '(lambda))))))

(define parse
  (lambda (m)
    (cond
      ((number? m)  `(&const ,m))
      ((eq? #t m)   `(&const true))
      ((eq? #f m)   `(&const false))
      ((name? m)    `(&var ,m))
      ((pair? m)    (cond 
                      ((eq? `lambda (car m))
                        (if (and (= 3 (length m))
                                 (list? (cadr m))
                                 (= 1 (length (cadr m)))
                                 (name? (caadr m)))
                            `(&lambda ,(cadr m) ,(parse (caddr m)))
                            (error 'parse "Syntax error")))
                      (else
                        `(&apply ,(parse (car m)) ,(parse (cadr m))))))
      (else         (error 'parse "Syntax error")))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                     Initial Type Environment
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define init_E
  '((add1 (int -> int)) (sub1 (int -> int))
    (zero? (int -> bool)) (not (bool -> bool))
    (and (bool -> (bool -> bool))) (or (bool -> (bool -> bool)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; driver
(define type_recons
  (lambda (m)
    (TR (parse m) init_E '())))

(define TR
  (lambda (ast E C)
    (car (recons ast E C))))
#|
"recons" returns a list containing the return type/type var and the current set
    of constraints.
|#
(define recons
  (lambda (e env constr)
    (cond
     ((eq? (car e) '&const) ; can use let for cdr e
      (cond
       ((eq? (cadr e) 'true)
       (list 'bool constr))
       ((eq? (cadr e) 'false)
       (list 'bool constr))
       ((number? (cadr e))
       (list 'int constr))))
     ((eq? (car e) '&var)
      (let ((a (lookup env (cadr e))))
	(if (null? a)
	    (let* ((b (newtvar))
		  (env (insert env (cadr e) b)))
	      (list b constr))
	    (list a constr))))
     ((eq? (car e) '&lambda)
      (if (recursive_type? e)
	  (error "recursive type")
	  (let* ((a (newtvar))
		(env (insert env (car (cadr e)) a)))
	    (let ((b (let ((param (car (cadr e)))
			   (arg (cadr (caddr e))))
		       (if (eq? param arg) ; lambda (x) x --> param = arg
			   a
			   (car (recons (caddr e) env constr))))))
	      (list `(,a -> ,b) constr)))))
     ((eq? (car e) '&apply)
      (let* ((c1 (recons (cadr e) env constr)) ; type1
	     (c2 (recons (caddr e) env (cadr c1))) ; type2
	     (c3 (unify (car (car c1)) (car c2) env (cadr c2))) ; unification
	     (rt (lookup_constr (caddr (car c1)) c3))) ; check if return type has been inferred
	     (list rt c3))))))

#|
"lookup_constr" looks up if the AST 'constr' has an entry for 'texp' and returns
    the type associated with it. If texp is a basic type or
unresolved yet, then it is returned as is.
|#

(define lookup_constr
  (lambda (texp constr)
    (cond
     ((null? constr)
      texp)
     ((eq? texp (car (car constr)))
      (car (cadr (car constr))))
     ((and (list? texp) (> (length texp) 1))
      (let* ((param_type (car texp))
	     (return_type (caddr texp))
	     (t1 (lookup_constr param_type constr))
	     (t2 (lookup_constr return_type constr)))
	(if (eq? return_type t1)
	    `(,t2 -> ,t1)
	    t2)))
     (else
      (lookup_constr texp (cdr constr))))))

#|
"unify" unifies 'type1' and 'type2' and produces a potentially new set of
    constraints. If unification fails, an error is reported.
|#
(define unify
  (lambda (type1 type2 env constr)
    (cond
     ((eq? type1 type2)
      constr)
     ((eq? #t (and (or (eq? type1 'int) (eq? type1 'bool)) (or (eq? type2 'int) (eq? type2 'bool))))
      (error 'unify "*** type conflict ***"))
     (else
      (if (or (eq? type1 'int) (eq? type1 'bool))
	  (insert constr type2 `(,type1))
	  (insert constr type1 `(,type2)))))))

#| for const functions:
      (let* ((fun_const (car (cadr e)))
	     (var_name (cdr (cadr e))) ; should already have a type
	     (var_type (lookup env var_name))
	     (arg_type (recons (car (caddr e)) env 0)))
	(if (eq? fun_const '&var)
	    (if (eq? (car var_type) arg_type) ;need to unify instead of comparing
		(caddr var_type)
		(error "error"))
	    (error "error2")))
      'apply))))

|#

#|
      ;; get function's type
      (let ((param_type (car (cadr e)))
	    (arg_type (caddr e))
	    (body_type (caddr (cadr e))))
	(if (eq? param_type arg_type)
	    param_type
;	    (error "Argument type doesn't match Parameter type")))
	    param_type))))))
|#

; returns the type of y if it exists in the env
(define lookup
  (lambda (env y)
    (cond
     ((null? env) env)
     ((eq? (car (car env)) y)
	 (cadr (car env)))
     (else (lookup (cdr env) y)))))

; inserts y with its type 't' in the env/constr
(define insert
  (lambda (env y t)
    (cons `(,y ,t) env)))

; checks if 'e' is a recursive type.
(define recursive_type?
  (lambda (e)
    (let* ((param (car (cadr e)))
	   (body (caddr e))
	   (b1 (car body)))
      (if (eq? b1 '&apply)
	  (let* ((b2 (cadr body))
		 (b3 (caddr body))
		 (var (cadr b2)))
	    (if (and (equal? b2 b3) (eq? var param))
		#t
		#f))
	  #f))))

; determines if 'type' is a basic type. returns boolean.
; it has no entry in env
#|(define basic_type?
  (lambda (type env)
    (eq? (lookup env type) '()))
|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                        Sample Test cases
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define M1 '((lambda (x) x) 5))
(define M2 '((lambda (x) (sub1 x)) 5))
(define M3 '((lambda (x) 1) ((lambda (x) (x x)) (lambda (x) (x x)))))
(define M4 '((lambda (x) ((and x) #f)) #t))

(define M5 1)
(define M6 #t)
(define M7 #f)
(define M8 'a)

;;; function abstraction
(define M9 'add1)
(define M10 '(lambda (x) 1))
(define M11 '(lambda (x) y))
(define M12 '(lambda (x) x))
(define M13 '(sub1 x)) ; (int) (application)
(define M14 '(lambda (x) (lambda (y) y)))
(define M15 '(lambda (x) (lambda (x) x)))
(define M16 '(lambda (x) (lambda (x) (lambda (x) 1))))
(define M17 '(lambda (x) (lambda (y) x)))


; application test-cases
(define M20 '((lambda (x) x) 5)) ; same as M1 (value as argument)
(define M21 '((lambda (x) x) y)) ;            (variable as argument)
(define M22 '((lambda (x) x) (lambda (x) 1))) ;(function as argument)
(define M23 '(lambda (x) (x x)))
(define M24 '((lambda (x) x) (lambda (y) y)))
(define M25 '((lambda (x) (lambda (y) x)) 5))
(define M26 '(add1 #t))

;;; write a function that runs all the above test cases
(define test_all
  (lambda ()
    (map type_recons `(,M1 ,M2 ,M4 ,M5 ,M6 ,M7 ,M8 ,M9 ,M10 ,M11 ,M12 ,M13 ,M14 ,M15 ,M16 ,M17 ,M20 ,M21 ,M22 ,M24 ,M25))))

#|
Results of test_all:
M1 int
M2 int
M4 bool
M5 int
M6 bool
M7 bool
M8 _a
M9 int -> int
M10 _a -> int
M11 _a -> _b
M12 _a -> _a
M13 int
M14 (_a1 -> (_a2 -> _a2))
M15 (_a1 -> (_a2 -> _a2))
M16 (_a1 -> (_a2 -> (_a3 -> int)))
M17 (_a1 -> (_a2 -> _a1))
M20 int
M21 _a
M22 _a -> int
M24 _a -> _a
M25 int

recursive types:
M3
M23

conflict:
M26
|#

#|
Todo:

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;
;;Tracing
;;;;;;;;;;;;;;;;;;;;;;;;;
(define trace_all
  (lambda ()
    (trace parse type_recons recons lookup_constr unify lookup insert recursive_type?)))
